Termination proof of /tmp/tmpboYqnf/FlattenTree.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBC2FIG (⇐)

↳2 FIGraph

↳3 FIGtoITRSProof (⇐)

↳4 AND

    ↳5 ITRS

        ↳6 DuplicateArgsRemoverProof (⇔)

        ↳7 ITRS

        ↳8 ITRStoQTRSProof (⇔)

        ↳9 QTRS

        ↳10 QTRSRRRProof (⇔)

        ↳11 QTRS

        ↳12 QTRSRRRProof (⇔)

        ↳13 QTRS

        ↳14 QTRSRRRProof (⇔)

        ↳15 QTRS

        ↳16 RisEmptyProof (⇔)

        ↳17 TRUE

    ↳18 ITRS

        ↳19 DuplicateArgsRemoverProof (⇔)

        ↳20 ITRS

        ↳21 ITRSFilterProcessorProof (⇐)

        ↳22 ITRS

        ↳23 ITRSFSMergerProof (⇐)

        ↳24 ITRS

        ↳25 ITRStoIDPProof (⇔)

        ↳26 IDP

        ↳27 UsableRulesProof (⇔)

        ↳28 IDP

        ↳29 ItpfGraphProof (⇔)

        ↳30 IDP

        ↳31 IDPNonInfProof (⇐)

        ↳32 AND

            ↳33 IDP

                ↳34 IDependencyGraphProof (⇔)

                ↳35 TRUE

            ↳36 IDP

                ↳37 IDependencyGraphProof (⇔)

                ↳38 TRUE

(0) Obligation:

JBC Problem based on JBC Program:

No human-readable program information known.

Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: FlattenTree

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 496 nodes with 2 SCCs.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

(4) Complex Obligation (AND)

(5) Obligation:

ITRS problem:

The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load3023(o1761, o1759) → NULL3243(o1761, o1759, o1759)
NULL3243(java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259)), java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259)), java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259))) → JMP8999(java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259)), java.lang.Object(Tree(o3001, java.lang.Object(Tree(o3002, o2258, NULL)), NULL)))
JMP8999(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL))) → Load3023(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL)))
NULL3243(o1883, java.lang.Object(Tree(java.lang.Object(Tree(o2987, o2988, o2989)), o2252, o2253)), java.lang.Object(Tree(java.lang.Object(Tree(o2987, o2988, o2989)), o2252, o2253))) → Load3023(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL)))
JMP6184(o1883, o2252) → Load3023(o1883, o2252)
NULL3243(o1883, java.lang.Object(Tree(NULL, o2252, o2253)), java.lang.Object(Tree(NULL, o2252, o2253))) → Load3023(o1883, o2252)
NULL3243(java.lang.Object(Tree(NULL, o2258, o2259)), java.lang.Object(Tree(NULL, o2258, o2259)), java.lang.Object(Tree(NULL, o2258, o2259))) → JMP6184(java.lang.Object(Tree(NULL, o2258, o2259)), o2258)
The set Q consists of the following terms:
Load3023(x0, x1)
JMP8999(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3, NULL)), NULL)))
NULL3243(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)), java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)))
JMP6184(x0, x1)
NULL3243(x0, java.lang.Object(Tree(NULL, x1, x2)), java.lang.Object(Tree(NULL, x1, x2)))

(6) DuplicateArgsRemoverProof (EQUIVALENT transformation)

Some arguments are removed because they only appear as duplicates.
We removed arguments according to the following replacements:

NULL3243(x1, x2, x3) → NULL3243(x1, x3)

(7) Obligation:

ITRS problem:

The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load3023(o1761, o1759) → NULL3243(o1761, o1759)
NULL3243(java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259)), java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259))) → JMP8999(java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259)), java.lang.Object(Tree(o3001, java.lang.Object(Tree(o3002, o2258, NULL)), NULL)))
JMP8999(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL))) → Load3023(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL)))
NULL3243(o1883, java.lang.Object(Tree(java.lang.Object(Tree(o2987, o2988, o2989)), o2252, o2253))) → Load3023(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL)))
JMP6184(o1883, o2252) → Load3023(o1883, o2252)
NULL3243(o1883, java.lang.Object(Tree(NULL, o2252, o2253))) → Load3023(o1883, o2252)
NULL3243(java.lang.Object(Tree(NULL, o2258, o2259)), java.lang.Object(Tree(NULL, o2258, o2259))) → JMP6184(java.lang.Object(Tree(NULL, o2258, o2259)), o2258)
The set Q consists of the following terms:
Load3023(x0, x1)
JMP8999(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3, NULL)), NULL)))
NULL3243(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)))
JMP6184(x0, x1)
NULL3243(x0, java.lang.Object(Tree(NULL, x1, x2)))

(8) ITRStoQTRSProof (EQUIVALENT transformation)

Represented integers and predefined function symbols by Terms

(9) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

Load3023(o1761, o1759) → NULL3243(o1761, o1759)
NULL3243(java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259)), java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259))) → JMP8999(java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259)), java.lang.Object(Tree(o3001, java.lang.Object(Tree(o3002, o2258, NULL)), NULL)))
JMP8999(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL))) → Load3023(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL)))
NULL3243(o1883, java.lang.Object(Tree(java.lang.Object(Tree(o2987, o2988, o2989)), o2252, o2253))) → Load3023(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL)))
JMP6184(o1883, o2252) → Load3023(o1883, o2252)
NULL3243(o1883, java.lang.Object(Tree(NULL, o2252, o2253))) → Load3023(o1883, o2252)
NULL3243(java.lang.Object(Tree(NULL, o2258, o2259)), java.lang.Object(Tree(NULL, o2258, o2259))) → JMP6184(java.lang.Object(Tree(NULL, o2258, o2259)), o2258)

The set Q consists of the following terms:

Load3023(x0, x1)
JMP8999(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3, NULL)), NULL)))
NULL3243(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)))
JMP6184(x0, x1)
NULL3243(x0, java.lang.Object(Tree(NULL, x1, x2)))

(10) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(JMP6184(x₁, x₂)) = 1 + x₁ + x₂
POL(JMP8999(x₁, x₂)) = x₁ + x₂
POL(Load3023(x₁, x₂)) = x₁ + x₂
POL(NULL) = 0
POL(NULL3243(x₁, x₂)) = x₁ + x₂
POL(Tree(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(java.lang.Object(x₁)) = 2 + x₁

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

JMP6184(o1883, o2252) → Load3023(o1883, o2252)
NULL3243(o1883, java.lang.Object(Tree(NULL, o2252, o2253))) → Load3023(o1883, o2252)
NULL3243(java.lang.Object(Tree(NULL, o2258, o2259)), java.lang.Object(Tree(NULL, o2258, o2259))) → JMP6184(java.lang.Object(Tree(NULL, o2258, o2259)), o2258)

(11) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

Load3023(o1761, o1759) → NULL3243(o1761, o1759)
NULL3243(java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259)), java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259))) → JMP8999(java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259)), java.lang.Object(Tree(o3001, java.lang.Object(Tree(o3002, o2258, NULL)), NULL)))
JMP8999(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL))) → Load3023(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL)))
NULL3243(o1883, java.lang.Object(Tree(java.lang.Object(Tree(o2987, o2988, o2989)), o2252, o2253))) → Load3023(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL)))

The set Q consists of the following terms:

Load3023(x0, x1)
JMP8999(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3, NULL)), NULL)))
NULL3243(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)))
JMP6184(x0, x1)
NULL3243(x0, java.lang.Object(Tree(NULL, x1, x2)))

(12) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(JMP8999(x₁, x₂)) = 2·x₁ + x₂
POL(Load3023(x₁, x₂)) = 2·x₁ + x₂
POL(NULL) = 0
POL(NULL3243(x₁, x₂)) = 2·x₁ + x₂
POL(Tree(x₁, x₂, x₃)) = 1 + 2·x₁ + x₂ + 2·x₃
POL(java.lang.Object(x₁)) = x₁

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

NULL3243(java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259)), java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259))) → JMP8999(java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259)), java.lang.Object(Tree(o3001, java.lang.Object(Tree(o3002, o2258, NULL)), NULL)))
NULL3243(o1883, java.lang.Object(Tree(java.lang.Object(Tree(o2987, o2988, o2989)), o2252, o2253))) → Load3023(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL)))

(13) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

Load3023(o1761, o1759) → NULL3243(o1761, o1759)
JMP8999(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL))) → Load3023(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL)))

The set Q consists of the following terms:

Load3023(x0, x1)
JMP8999(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3, NULL)), NULL)))
NULL3243(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)))
JMP6184(x0, x1)
NULL3243(x0, java.lang.Object(Tree(NULL, x1, x2)))

(14) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(JMP8999(x₁, x₂)) = 2 + x₁ + x₂
POL(Load3023(x₁, x₂)) = 1 + x₁ + x₂
POL(NULL) = 0
POL(NULL3243(x₁, x₂)) = x₁ + x₂
POL(Tree(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(java.lang.Object(x₁)) = x₁

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

Load3023(o1761, o1759) → NULL3243(o1761, o1759)
JMP8999(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL))) → Load3023(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL)))

(15) Obligation:

Q restricted rewrite system:
R is empty.
The set Q consists of the following terms:

Load3023(x0, x1)
JMP8999(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3, NULL)), NULL)))
NULL3243(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)))
JMP6184(x0, x1)
NULL3243(x0, java.lang.Object(Tree(NULL, x1, x2)))

(16) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(17) TRUE

(18) Obligation:

ITRS problem:

The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC)))) → Load9325ARR1(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Load9325ARR1(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Cond_Load9325ARR1(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Cond_Load9325ARR1(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)))
JMP11303(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2))) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)), o6813, o6814))) → Load9325ARR2(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR2(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR2(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR2(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)))
Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2))) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i843, i826 + -1, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)), o6807))) → Load9325ARR3(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Load9325ARR3(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Cond_Load9325ARR3(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Cond_Load9325ARR3(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826 + -1, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)))
Inc13311(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC)))) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i843, i826 + -1, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))))
JMP13217(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC)))) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i843, i826 + -1, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, NULL, o6807))) → Load9325ARR4(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, NULL, o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Load9325ARR4(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Cond_Load9325ARR4(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Cond_Load9325ARR4(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826 + -1, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC)))) → Load9325ARR5(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR5(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR5(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR5(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → JMP11303(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826, java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)))
JMP13263(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC)))) → Inc13311(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, o6813, o6814))) → Load9325ARR6(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR6(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR6(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR6(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Inc13311(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, NULL, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, NULL, java.lang.Object(EOC)))) → Load9325ARR7(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, NULL, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, NULL, java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Load9325ARR7(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(Tree(o6453, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Cond_Load9325ARR7(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(Tree(o6453, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Cond_Load9325ARR7(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(Tree(o6453, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → JMP13217(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(Tree(o6453, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(NULL, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, o6454, java.lang.Object(EOC)))) → Load9325ARR8(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(NULL, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR8(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR8(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR8(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → JMP13263(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6454, java.lang.Object(EOC))))
The set Q consists of the following terms:
Load9325ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, java.lang.Object(Tree(x5, x6, x7)), java.lang.Object(EOC))), java.lang.Object(Tree(x4, java.lang.Object(Tree(x5, x6, x7)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, x8, x9, x10)))
Cond_Load9325ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, java.lang.Object(Tree(x5, x6, x7)), java.lang.Object(EOC))), java.lang.Object(Tree(x4, java.lang.Object(Tree(x5, x6, x7)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, x8, x9, x10)))
JMP11303(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, x7, x8)))
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(x6, x7, x8)), x9, x10)))
Load9325ARR2(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(x6, x7, x8)), x9, x10)), java.lang.Object(java.lang.String(x11, x12, x13, x14)))
Cond_Load9325ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(x6, x7, x8)), x9, x10)), java.lang.Object(java.lang.String(x11, x12, x13, x14)))
Inc11229(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, x7, x8)))
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(x7, x8, x9)), x10)))
Load9325ARR3(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(x7, x8, x9)), x10)), java.lang.Object(java.lang.String(0, x11, x12, x13)))
Cond_Load9325ARR3(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(x7, x8, x9)), x10)), java.lang.Object(java.lang.String(0, x11, x12, x13)))
Inc13311(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))))
JMP13217(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, NULL, x7)))
Load9325ARR4(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x7)), java.lang.Object(java.lang.String(0, x8, x9, x10)))
Cond_Load9325ARR4(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x7)), java.lang.Object(java.lang.String(0, x8, x9, x10)))
Load9325ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(java.lang.Object(Tree(x4, x5, x6)), x7, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(x4, x5, x6)), x7, java.lang.Object(EOC))), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Cond_Load9325ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(java.lang.Object(Tree(x4, x5, x6)), x7, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(x4, x5, x6)), x7, java.lang.Object(EOC))), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
JMP13263(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, x6, x7)))
Load9325ARR6(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x6, x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Cond_Load9325ARR6(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x6, x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Load9325ARR7(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(Tree(x4, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, x5, x6, x7)))
Cond_Load9325ARR7(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(Tree(x4, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, x5, x6, x7)))
Load9325ARR8(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x4, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x4, java.lang.Object(EOC))), java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load9325ARR8(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x4, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x4, java.lang.Object(EOC))), java.lang.Object(java.lang.String(x5, x6, x7, x8)))

(19) DuplicateArgsRemoverProof (EQUIVALENT transformation)

Some arguments are removed because they only appear as duplicates.
We removed arguments according to the following replacements:

JMP13263(x1, x2, x3, x4, x5) → JMP13263(x1, x2, x3, x5)
Cond_Load9325ARR8(x1, x2, x3, x4, x5, x6, x7) → Cond_Load9325ARR8(x1, x2, x3, x4, x6, x7)
Load9325ARR8(x1, x2, x3, x4, x5, x6) → Load9325ARR8(x1, x2, x3, x5, x6)
JMP13217(x1, x2, x3, x4, x5) → JMP13217(x1, x2, x3, x5)
Cond_Load9325ARR7(x1, x2, x3, x4, x5, x6, x7) → Cond_Load9325ARR7(x1, x2, x3, x4, x6, x7)
Load9325ARR7(x1, x2, x3, x4, x5, x6) → Load9325ARR7(x1, x2, x3, x5, x6)
Inc13311(x1, x2, x3, x4, x5) → Inc13311(x1, x2, x3, x5)
Cond_Load9325ARR5(x1, x2, x3, x4, x5, x6, x7) → Cond_Load9325ARR5(x1, x2, x3, x4, x6, x7)
Load9325ARR5(x1, x2, x3, x4, x5, x6) → Load9325ARR5(x1, x2, x3, x5, x6)
Cond_Load9325ARR1(x1, x2, x3, x4, x5, x6, x7) → Cond_Load9325ARR1(x1, x2, x3, x4, x6, x7)
Load9325ARR1(x1, x2, x3, x4, x5, x6) → Load9325ARR1(x1, x2, x3, x5, x6)

(20) Obligation:

ITRS problem:

The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC)))) → Load9325ARR1(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Load9325ARR1(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Cond_Load9325ARR1(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Cond_Load9325ARR1(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)))
JMP11303(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2))) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)), o6813, o6814))) → Load9325ARR2(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR2(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR2(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR2(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)))
Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2))) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i843, i826 + -1, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)), o6807))) → Load9325ARR3(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Load9325ARR3(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Cond_Load9325ARR3(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Cond_Load9325ARR3(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826 + -1, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)))
Inc13311(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC)))) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i843, i826 + -1, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))))
JMP13217(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC)))) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i843, i826 + -1, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, NULL, o6807))) → Load9325ARR4(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, NULL, o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Load9325ARR4(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Cond_Load9325ARR4(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Cond_Load9325ARR4(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826 + -1, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC)))) → Load9325ARR5(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR5(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR5(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR5(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → JMP11303(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826, java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)))
JMP13263(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC)))) → Inc13311(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, o6813, o6814))) → Load9325ARR6(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR6(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR6(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR6(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Inc13311(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, NULL, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, NULL, java.lang.Object(EOC)))) → Load9325ARR7(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, NULL, java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Load9325ARR7(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Cond_Load9325ARR7(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Cond_Load9325ARR7(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → JMP13217(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(NULL, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, o6454, java.lang.Object(EOC)))) → Load9325ARR8(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(NULL, o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR8(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR8(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR8(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → JMP13263(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6454, java.lang.Object(EOC))))
The set Q consists of the following terms:
Load9325ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, java.lang.Object(Tree(x5, x6, x7)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, x8, x9, x10)))
Cond_Load9325ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, java.lang.Object(Tree(x5, x6, x7)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, x8, x9, x10)))
JMP11303(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, x7, x8)))
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(x6, x7, x8)), x9, x10)))
Load9325ARR2(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(x6, x7, x8)), x9, x10)), java.lang.Object(java.lang.String(x11, x12, x13, x14)))
Cond_Load9325ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(x6, x7, x8)), x9, x10)), java.lang.Object(java.lang.String(x11, x12, x13, x14)))
Inc11229(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, x7, x8)))
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(x7, x8, x9)), x10)))
Load9325ARR3(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(x7, x8, x9)), x10)), java.lang.Object(java.lang.String(0, x11, x12, x13)))
Cond_Load9325ARR3(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(x7, x8, x9)), x10)), java.lang.Object(java.lang.String(0, x11, x12, x13)))
Inc13311(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))))
JMP13217(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, NULL, x7)))
Load9325ARR4(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x7)), java.lang.Object(java.lang.String(0, x8, x9, x10)))
Cond_Load9325ARR4(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x7)), java.lang.Object(java.lang.String(0, x8, x9, x10)))
Load9325ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(java.lang.Object(Tree(x4, x5, x6)), x7, java.lang.Object(EOC))), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Cond_Load9325ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(java.lang.Object(Tree(x4, x5, x6)), x7, java.lang.Object(EOC))), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
JMP13263(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, x6, x7)))
Load9325ARR6(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x6, x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Cond_Load9325ARR6(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x6, x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Load9325ARR7(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, x5, x6, x7)))
Cond_Load9325ARR7(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, x5, x6, x7)))
Load9325ARR8(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x4, java.lang.Object(EOC))), java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load9325ARR8(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x4, java.lang.Object(EOC))), java.lang.Object(java.lang.String(x5, x6, x7, x8)))

(21) ITRSFilterProcessorProof (SOUND transformation)

We filter according the heuristic IdpCand1ShapeHeuristic
We removed arguments according to the following replacements:

Load9325(x1, x2, x3, x4, x5) → Load9325(x1, x2, x3)
Tree(x1, x2, x3) → Tree
Load9325ARR1(x1, x2, x3, x4, x5) → Load9325ARR1(x1, x2, x3)
Cond_Load9325ARR1(x1, x2, x3, x4, x5, x6) → Cond_Load9325ARR1(x1, x2, x3, x4)
Inc11229(x1, x2, x3, x4, x5) → Inc11229(x1, x2, x3)
JMP11303(x1, x2, x3, x4, x5) → JMP11303(x1, x2, x3)
Load9325ARR2(x1, x2, x3, x4, x5, x6) → Load9325ARR2(x1, x2, x3, x6)
Cond_Load9325ARR2(x1, x2, x3, x4, x5, x6, x7) → Cond_Load9325ARR2(x1, x2, x3, x4, x7)
Load9325ARR3(x1, x2, x3, x4, x5, x6) → Load9325ARR3(x1, x2, x3)
Cond_Load9325ARR3(x1, x2, x3, x4, x5, x6, x7) → Cond_Load9325ARR3(x1, x2, x3, x4)
Inc13311(x1, x2, x3, x4) → Inc13311(x1, x2, x3)
JMP13217(x1, x2, x3, x4) → JMP13217(x1, x2, x3)
Load9325ARR4(x1, x2, x3, x4, x5, x6) → Load9325ARR4(x1, x2, x3)
Cond_Load9325ARR4(x1, x2, x3, x4, x5, x6, x7) → Cond_Load9325ARR4(x1, x2, x3, x4)
Load9325ARR5(x1, x2, x3, x4, x5) → Load9325ARR5(x1, x2, x3, x5)
Cond_Load9325ARR5(x1, x2, x3, x4, x5, x6) → Cond_Load9325ARR5(x1, x2, x3, x4, x6)
JMP13263(x1, x2, x3, x4) → JMP13263(x1, x2, x3)
Load9325ARR6(x1, x2, x3, x4, x5, x6) → Load9325ARR6(x1, x2, x3, x6)
Cond_Load9325ARR6(x1, x2, x3, x4, x5, x6, x7) → Cond_Load9325ARR6(x1, x2, x3, x4, x7)
Load9325ARR7(x1, x2, x3, x4, x5) → Load9325ARR7(x1, x2, x3)
Cond_Load9325ARR7(x1, x2, x3, x4, x5, x6) → Cond_Load9325ARR7(x1, x2, x3, x4)
Load9325ARR8(x1, x2, x3, x4, x5) → Load9325ARR8(x1, x2, x3, x5)
Cond_Load9325ARR8(x1, x2, x3, x4, x5, x6) → Cond_Load9325ARR8(x1, x2, x3, x4, x6)

(22) Obligation:

ITRS problem:

The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR1(java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Load9325ARR1(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Cond_Load9325ARR1(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Cond_Load9325ARR1(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826)
JMP11303(java.lang.Object(ARRAY(i2, a4262data)), i843, i826) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i843, i826)
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR2(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR2(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR2(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR2(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826)
Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i843, i826) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i843, i826 + -1)
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR3(java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Load9325ARR3(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Cond_Load9325ARR3(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Cond_Load9325ARR3(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826 + -1)
Inc13311(java.lang.Object(ARRAY(i2, a4262data)), i843, i826) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i843, i826 + -1)
JMP13217(java.lang.Object(ARRAY(i2, a4262data)), i843, i826) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i843, i826 + -1)
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR4(java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Load9325ARR4(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Cond_Load9325ARR4(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Cond_Load9325ARR4(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826 + -1)
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR5(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR5(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR5(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR5(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → JMP11303(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826)
JMP13263(java.lang.Object(ARRAY(i2, a4262data)), i843, i826) → Inc13311(java.lang.Object(ARRAY(i2, a4262data)), i843, i826)
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR6(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR6(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR6(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR6(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Inc13311(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826)
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR7(java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Load9325ARR7(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Cond_Load9325ARR7(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Cond_Load9325ARR7(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → JMP13217(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826)
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR8(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR8(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR8(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR8(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → JMP13263(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826)
The set Q consists of the following terms:
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load9325ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
JMP11303(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR2(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load9325ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Inc11229(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR3(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load9325ARR3(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Inc13311(java.lang.Object(ARRAY(x0, x1)), x2, x3)
JMP13217(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR4(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load9325ARR4(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load9325ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
JMP13263(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR6(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load9325ARR6(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Load9325ARR7(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load9325ARR7(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR8(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load9325ARR8(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

(23) ITRSFSMergerProof (SOUND transformation)

The following function symbols have been merged:

Load9325ARR1, Load9325ARR7	>	Load9325ARR1_3
Load9325ARR3, Load9325ARR4	>	Load9325ARR3_3
Cond_Load9325ARR1, Cond_Load9325ARR7	>	Cond_Load9325ARR1_4
JMP11303, JMP13263	>	JMP11303_3
Load9325ARR2, Load9325ARR6	>	Load9325ARR2_4
Load9325ARR5, Load9325ARR8	>	Load9325ARR5_4
Cond_Load9325ARR5, Cond_Load9325ARR8	>	Cond_Load9325ARR5_5
Cond_Load9325ARR2, Cond_Load9325ARR6	>	Cond_Load9325ARR2_5
Inc11229, Inc13311, JMP13217	>	Inc11229_3
Cond_Load9325ARR3, Cond_Load9325ARR4	>	Cond_Load9325ARR3_4

(24) Obligation:

ITRS problem:

The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

(25) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(26) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

The ITRS R consists of the following rules:
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR1(java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Load9325ARR1(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Cond_Load9325ARR1(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Cond_Load9325ARR1(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826)
JMP11303(java.lang.Object(ARRAY(i2, a4262data)), i843, i826) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i843, i826)
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR2(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR2(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR2(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR2(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826)
Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i843, i826) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i843, i826 + -1)
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR3(java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Load9325ARR3(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Cond_Load9325ARR3(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Cond_Load9325ARR3(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826 + -1)
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR5(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR5(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR5(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR5(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → JMP11303(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826)

The integer pair graph contains the following rules and edges:
(0): LOAD9325(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0]) → LOAD9325ARR1(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0])
(1): LOAD9325ARR1(java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1]) → COND_LOAD9325ARR1(i824[1] > 0 && i824[1] < i2[1] && i826[1] > 0 && i824[1] + 1 > 0, java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1])
(2): COND_LOAD9325ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a4262data[2])), i824[2], i826[2]) → INC11229(java.lang.Object(ARRAY(i2[2], a4262data[2])), i824[2] + 1, i826[2])
(3): JMP11303'(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3]) → INC11229(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3])
(4): LOAD9325(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4]) → LOAD9325ARR2(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4], java.lang.Object(java.lang.String(i901[4], i862[4], i864[4], a4416[4])))
(5): LOAD9325ARR2(java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5]))) → COND_LOAD9325ARR2(i901[5] > 0 && i824[5] > 0 && i824[5] < i2[5] && i826[5] > 0 && i824[5] + 1 > 0, java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))
(6): COND_LOAD9325ARR2(TRUE, java.lang.Object(ARRAY(i2[6], a4262data[6])), i824[6], i826[6], java.lang.Object(java.lang.String(i901[6], i862[6], i864[6], a4416[6]))) → INC11229(java.lang.Object(ARRAY(i2[6], a4262data[6])), i824[6] + 1, i826[6])
(7): INC11229(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], i826[7]) → LOAD9325(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], i826[7] + -1)
(8): LOAD9325(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8]) → LOAD9325ARR3(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8])
(9): LOAD9325ARR3(java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9]) → COND_LOAD9325ARR3(i824[9] > 0 && i824[9] < i2[9] && i826[9] > 0 && i824[9] + 1 > 0, java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9])
(10): COND_LOAD9325ARR3(TRUE, java.lang.Object(ARRAY(i2[10], a4262data[10])), i824[10], i826[10]) → LOAD9325(java.lang.Object(ARRAY(i2[10], a4262data[10])), i824[10] + 1, i826[10] + -1)
(11): LOAD9325(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11]) → LOAD9325ARR5(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11], java.lang.Object(java.lang.String(i901[11], i862[11], i864[11], a4416[11])))
(12): LOAD9325ARR5(java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12]))) → COND_LOAD9325ARR5(i901[12] > 0 && i824[12] > 0 && i824[12] < i2[12] && i826[12] > 0 && i824[12] + 1 > 0, java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))
(13): COND_LOAD9325ARR5(TRUE, java.lang.Object(ARRAY(i2[13], a4262data[13])), i824[13], i826[13], java.lang.Object(java.lang.String(i901[13], i862[13], i864[13], a4416[13]))) → JMP11303'(java.lang.Object(ARRAY(i2[13], a4262data[13])), i824[13] + 1, i826[13])

(0) -> (1), if ((i824[0] →^* i824[1])∧(java.lang.Object(ARRAY(i2[0], a4262data[0])) →^* java.lang.Object(ARRAY(i2[1], a4262data[1])))∧(i826[0] →^* i826[1]))

(1) -> (2), if ((i826[1] →^* i826[2])∧(i824[1] →^* i824[2])∧(i824[1] > 0 && i824[1] < i2[1] && i826[1] > 0 && i824[1] + 1 > 0 →^* TRUE)∧(java.lang.Object(ARRAY(i2[1], a4262data[1])) →^* java.lang.Object(ARRAY(i2[2], a4262data[2]))))

(2) -> (7), if ((java.lang.Object(ARRAY(i2[2], a4262data[2])) →^* java.lang.Object(ARRAY(i2[7], a4262data[7])))∧(i824[2] + 1 →^* i843[7])∧(i826[2] →^* i826[7]))

(3) -> (7), if ((i843[3] →^* i843[7])∧(java.lang.Object(ARRAY(i2[3], a4262data[3])) →^* java.lang.Object(ARRAY(i2[7], a4262data[7])))∧(i826[3] →^* i826[7]))

(4) -> (5), if ((java.lang.Object(java.lang.String(i901[4], i862[4], i864[4], a4416[4])) →^* java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))∧(i824[4] →^* i824[5])∧(java.lang.Object(ARRAY(i2[4], a4262data[4])) →^* java.lang.Object(ARRAY(i2[5], a4262data[5])))∧(i826[4] →^* i826[5]))

(5) -> (6), if ((i826[5] →^* i826[6])∧(java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])) →^* java.lang.Object(java.lang.String(i901[6], i862[6], i864[6], a4416[6])))∧(i824[5] →^* i824[6])∧(java.lang.Object(ARRAY(i2[5], a4262data[5])) →^* java.lang.Object(ARRAY(i2[6], a4262data[6])))∧(i901[5] > 0 && i824[5] > 0 && i824[5] < i2[5] && i826[5] > 0 && i824[5] + 1 > 0 →^* TRUE))

(6) -> (7), if ((i826[6] →^* i826[7])∧(i824[6] + 1 →^* i843[7])∧(java.lang.Object(ARRAY(i2[6], a4262data[6])) →^* java.lang.Object(ARRAY(i2[7], a4262data[7]))))

(7) -> (0), if ((i826[7] + -1 →^* i826[0])∧(java.lang.Object(ARRAY(i2[7], a4262data[7])) →^* java.lang.Object(ARRAY(i2[0], a4262data[0])))∧(i843[7] →^* i824[0]))

(7) -> (4), if ((i843[7] →^* i824[4])∧(i826[7] + -1 →^* i826[4])∧(java.lang.Object(ARRAY(i2[7], a4262data[7])) →^* java.lang.Object(ARRAY(i2[4], a4262data[4]))))

(7) -> (8), if ((i826[7] + -1 →^* i826[8])∧(java.lang.Object(ARRAY(i2[7], a4262data[7])) →^* java.lang.Object(ARRAY(i2[8], a4262data[8])))∧(i843[7] →^* i824[8]))

(7) -> (11), if ((i843[7] →^* i824[11])∧(java.lang.Object(ARRAY(i2[7], a4262data[7])) →^* java.lang.Object(ARRAY(i2[11], a4262data[11])))∧(i826[7] + -1 →^* i826[11]))

(8) -> (9), if ((java.lang.Object(ARRAY(i2[8], a4262data[8])) →^* java.lang.Object(ARRAY(i2[9], a4262data[9])))∧(i826[8] →^* i826[9])∧(i824[8] →^* i824[9]))

(9) -> (10), if ((i826[9] →^* i826[10])∧(i824[9] > 0 && i824[9] < i2[9] && i826[9] > 0 && i824[9] + 1 > 0 →^* TRUE)∧(i824[9] →^* i824[10])∧(java.lang.Object(ARRAY(i2[9], a4262data[9])) →^* java.lang.Object(ARRAY(i2[10], a4262data[10]))))

(10) -> (0), if ((java.lang.Object(ARRAY(i2[10], a4262data[10])) →^* java.lang.Object(ARRAY(i2[0], a4262data[0])))∧(i824[10] + 1 →^* i824[0])∧(i826[10] + -1 →^* i826[0]))

(10) -> (4), if ((i824[10] + 1 →^* i824[4])∧(java.lang.Object(ARRAY(i2[10], a4262data[10])) →^* java.lang.Object(ARRAY(i2[4], a4262data[4])))∧(i826[10] + -1 →^* i826[4]))

(10) -> (8), if ((i824[10] + 1 →^* i824[8])∧(java.lang.Object(ARRAY(i2[10], a4262data[10])) →^* java.lang.Object(ARRAY(i2[8], a4262data[8])))∧(i826[10] + -1 →^* i826[8]))

(10) -> (11), if ((i826[10] + -1 →^* i826[11])∧(java.lang.Object(ARRAY(i2[10], a4262data[10])) →^* java.lang.Object(ARRAY(i2[11], a4262data[11])))∧(i824[10] + 1 →^* i824[11]))

(11) -> (12), if ((i824[11] →^* i824[12])∧(java.lang.Object(ARRAY(i2[11], a4262data[11])) →^* java.lang.Object(ARRAY(i2[12], a4262data[12])))∧(i826[11] →^* i826[12])∧(java.lang.Object(java.lang.String(i901[11], i862[11], i864[11], a4416[11])) →^* java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12]))))

(12) -> (13), if ((i901[12] > 0 && i824[12] > 0 && i824[12] < i2[12] && i826[12] > 0 && i824[12] + 1 > 0 →^* TRUE)∧(java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])) →^* java.lang.Object(java.lang.String(i901[13], i862[13], i864[13], a4416[13])))∧(i824[12] →^* i824[13])∧(java.lang.Object(ARRAY(i2[12], a4262data[12])) →^* java.lang.Object(ARRAY(i2[13], a4262data[13])))∧(i826[12] →^* i826[13]))

(13) -> (3), if ((java.lang.Object(ARRAY(i2[13], a4262data[13])) →^* java.lang.Object(ARRAY(i2[3], a4262data[3])))∧(i824[13] + 1 →^* i843[3])∧(i826[13] →^* i826[3]))

The set Q consists of the following terms:
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load9325ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
JMP11303(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR2(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load9325ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Inc11229(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR3(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load9325ARR3(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load9325ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

(27) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(28) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD9325(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0]) → LOAD9325ARR1(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0])
(1): LOAD9325ARR1(java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1]) → COND_LOAD9325ARR1(i824[1] > 0 && i824[1] < i2[1] && i826[1] > 0 && i824[1] + 1 > 0, java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1])
(2): COND_LOAD9325ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a4262data[2])), i824[2], i826[2]) → INC11229(java.lang.Object(ARRAY(i2[2], a4262data[2])), i824[2] + 1, i826[2])
(3): JMP11303'(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3]) → INC11229(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3])
(4): LOAD9325(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4]) → LOAD9325ARR2(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4], java.lang.Object(java.lang.String(i901[4], i862[4], i864[4], a4416[4])))
(5): LOAD9325ARR2(java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5]))) → COND_LOAD9325ARR2(i901[5] > 0 && i824[5] > 0 && i824[5] < i2[5] && i826[5] > 0 && i824[5] + 1 > 0, java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))
(6): COND_LOAD9325ARR2(TRUE, java.lang.Object(ARRAY(i2[6], a4262data[6])), i824[6], i826[6], java.lang.Object(java.lang.String(i901[6], i862[6], i864[6], a4416[6]))) → INC11229(java.lang.Object(ARRAY(i2[6], a4262data[6])), i824[6] + 1, i826[6])
(7): INC11229(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], i826[7]) → LOAD9325(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], i826[7] + -1)
(8): LOAD9325(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8]) → LOAD9325ARR3(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8])
(9): LOAD9325ARR3(java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9]) → COND_LOAD9325ARR3(i824[9] > 0 && i824[9] < i2[9] && i826[9] > 0 && i824[9] + 1 > 0, java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9])
(10): COND_LOAD9325ARR3(TRUE, java.lang.Object(ARRAY(i2[10], a4262data[10])), i824[10], i826[10]) → LOAD9325(java.lang.Object(ARRAY(i2[10], a4262data[10])), i824[10] + 1, i826[10] + -1)
(11): LOAD9325(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11]) → LOAD9325ARR5(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11], java.lang.Object(java.lang.String(i901[11], i862[11], i864[11], a4416[11])))
(12): LOAD9325ARR5(java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12]))) → COND_LOAD9325ARR5(i901[12] > 0 && i824[12] > 0 && i824[12] < i2[12] && i826[12] > 0 && i824[12] + 1 > 0, java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))
(13): COND_LOAD9325ARR5(TRUE, java.lang.Object(ARRAY(i2[13], a4262data[13])), i824[13], i826[13], java.lang.Object(java.lang.String(i901[13], i862[13], i864[13], a4416[13]))) → JMP11303'(java.lang.Object(ARRAY(i2[13], a4262data[13])), i824[13] + 1, i826[13])